\begin{tabbing}
w{-}match($w$; $l$; $t$; ${\it t'}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\parallel$w{-}snds($w$; $l$; $t$)$\parallel$ $\leq$z $\parallel$w{-}rcvs($w$; $l$; ${\it t'}$)$\parallel$\+
\\[0ex]$\wedge_{b}$ $\parallel$w{-}rcvs($w$; $l$; ${\it t'}$)$\parallel$ $<$z ($\parallel$w{-}snds($w$; $l$; $t$)$\parallel$+$\parallel$onlnk($l$;w{-}m($w$; source($l$); $t$))$\parallel$)
\-
\end{tabbing}